$\forall$$A$:Type, $d$:EqDecider($A$), $i$, $j$:$A$. $i$ $=$ $j$ $\Rightarrow$ ((eqof($d$)($i$,$j$)) $\sim$ true$_{2}$)